ALC or K.

We already thought that this is correct,

that means that every formula or label has a successful table.

What is missing is the inversion.

The inversion of correctness is always completeness.

If I have a table knot N, which is successful according to our AND-OR definition,

that is, if it is an OR-knot, it has a successful child,

if it is an AND-knot, it has only successful children,

then its label, a formula L of N, is achievable.

So this is the usual deformation of completeness.

In non-table cases, this is always the case,

in any case in the absence of negation,

that one reduces the veracity to completeness.

And then from the completeness set,

every syntactically consistent formula is achievable.

In this case, syntactically consistent means that it has a successful table.

If I put it on my head and convert the table into a sequence proof,

then it means that the search for a proof for the opposite of my target formula fails.

So we have to show completeness, that means we have to build a model.

So in the rough, it is relatively clear what happens.

We had last time considered in our example what the states of the model are,

that we extract from such a table.

And these are the states of the successful AND-knot.

We had last time considered in our example that this is probably the case.

What does this look like in general?

A successful AND-knot, so it is a first AND-knot.

It has some positive propositional stuff.

A AND-knot is propositional saturated,

it does not contain any propositional material,

only top-level, it contains only atoms, negated atoms, boxes and negated boxes.

I can list everything, I have here some positive atoms, I have some negative atoms,

positive atoms q1 to qn, negative atoms not p1 to not pk,

positive boxes box phi1 to box phin,

and also negative boxes not psi1 to not psi,

there is even a letter over L.

So this is now a AND-knot.

And that it is successful means that for every rule application on this thing,

and rule applications are now always applications of the non-box rule,

because other rules are no longer applicable by definition of an AND-knot,

I get a child here, what would be the first child?

Each of these children gets by definition all boxed formulas with phi1 to phin,

and then it gets, well, I have here L different applications of the non-box rule,

because I have L negated boxes,

and every time I get exactly here the formula under the negated box as the only one

still in the middle of the formulas under the positive boxes,

so here for example psi1, so you can guess here,

so L successors, so it goes here to L.

Oh yes, I wanted to write M once, I think I'll do some M here.

Yes, the numbers are of course potentially different.

So, and then at the moment here the induction requirement is applied,